00100	               THE MCCARTHY AIRLINE RESERVATION SYSTEM
00200	
00300	
00400		The  McCarthy  airline reservation system serves the McCarthy
00500	Airline which has exactly one seat on its  one  airplane  that  never
00600	flies.    The  airline has two customers, Ed and Zohar, who prefer it
00700	to other airlines because of its perfect safety record.    Every  now
00800	and  then,  Ed  or  Zohar  call  up  to reserve a seat or to cancel a
00900	reservation.  The reservation system should accept a  reservation  if
01000	the  seat  is free, replying "ok", and it should say "no" if the seat
01100	is not available. It should accept a cancellation  replying  "ok"  if
01200	the seat is currently reserved by the person attempting to cancel it,
01300	and otherwise should reply "no".
01400	
01500		The behavior of Ed is described by the algolish program
01600	
01700	Ed:	wait a while;
01800		i ← amb(1,-1);
01900		wait for acceptance;
02000		go to Ed;
02100	
02200	Here  amb(-1,1)  means  that  -1  or 1 is chosen indeterminately, and
02300	"wait for acceptance" waits till the reservation system  accepts  the
02400	input i.  Similarly, Zohar is described by the program
02500	
02600	Zohar:	wait a while;
02700		i ← amb(2,-2);
02800		wait for acceptance;
02900		go to Zohar;
03000	
03100		The reservation system itself is described by the program
03200	
03300	start:	h ← 0;
03400	loop:	wait for input;
03500		if h = 0 then begin
03600			if i > 0 then begin
03700				h ← i; o ← "ok"; go to loop end;
03800			else  begin o ← "no"; go to loop end end;
03900		if i = -h then begin h ← 0; o ← "ok"; go to loop end;
04000		o ← "no";
04100		go to loop;
04200	
04300		Our problem is to express the correctness of the McCarthy
04400	airline reservation system as a formula of first order logic using
04500	methods of Manna and Ashcroft.  To do this we introduce the notion
04600	of a refereee program.  This program starts with a counter initialized
04700	with some non-negative integer N and a variable hr initialized to 0.
04800	Every time Ed or Zohar attempts to reserve a seat or cancel a reservation,
04900	the referee looks for a response from the reservation system.  It 
05000	checks this response against its own idea of the state of the seat.
05100	If it disagrees with the action it stops the whole process and
05200	sets a variable named result to "lose".  If it agrees with the action,
05300	then it counts n down by 1 unless n=0 in which case it terminates
05400	the program setting result to "win".  
05500	
05600		The correctness of the reservation system is expressed by the
05700	assertion that for every value of N, the referee will eventually 
05800	terminate  with %result%=%"win".  Note that the system consisting
05900	of the reservation system and its customers is non-terminating.
06000	The system consisting of the reservation system, the two customers,
06100	and the referee is a parallel indeterminate program as treated
06200	in (Ashcroft and Manna 1970), and its correct termination can be
06300	expressed as a formula of first order logic by their methods.
06400	
06500		In the present simple case, the referee program is virtually
06600	a copy of the reservation system, but this need not be the case
06700	in general for the following reasons:
06800	
06900		1. While the referee program has to keep track of the computation,
07000	it doesn't have to be efficient since it is present only for
07100	mathematical reasons.
07200	
07300		2. The referee program can include quantifiers in its conditions,
07400	choices of members from sets, etc.  In fact, it can contain any
07500	terms axiomatizable in first order logic even if they are not
07600	computable per se.  This only results in complicating the logical
07700	formula expressing the correctness of the program without taking
07800	it out of first order logic.
07900	
08000		3. It may be that the property one wants to prove about the
08100	system says less than a complete specification of all its outputs.
08200	In this case, the referee program and the correctness formula may
08300	be simpler than otherwise.
08400	
08500		In the present case, the referee program may be written
08600	as follows:
08700	
08800	Scott:	n ← N; hr ← 0;
08900	rloop:	if n = 0 then begin result ← "win"; go to done;
09000		customer ← amb(Ed,Zohar);
09100		wait for i;
09200	
09300	
09400	
09500	
09600	
09700	FALL BACK AND REGROUP
09800	
09900		Let us consider more elementary handshaking protocols.
10000	
10100	1. Suppose we have a sender and a receiver wherein the receiver is
10200	guaranteed to be fast enough.  The receiver program is then
10300	
10350	begin
10400	rloop:	wait for ¬on;
10500		wait for on;
10600		if s ≠ end then begin b[i] ← s; i ← i + 1; go to rloop end
10700	end.
10800	
10900	The corresponding sender program is
11000	
11050	begin
11100	sloop:	on ← false;
11200		wait 1;
11300		if i > n then go to finish;
11400		s ← a[i]; i ← i+1;
11500		on ← true;
11600		wait 1;
11700		go to sloop;
11800	finish:
11900	end.
12000	
12100	
12200		A better way (thanks to Dave Poole) is
12300	
12400	comment Program for sender;
12500	begin
12600	sloop:	wait for ¬on;
12700		s ← a[i]; i ← i+1; if i = n then go to finish;
12800		on ← true;
12900		go to sloop;
13000	end.
13100	
13200	comment  Program for receiver;
13300	begin
13400	rloop:	wait for on;
13500		b[i] ← s; i ← i+1;
13600		on ← true;
13700		go to rloop;
13800	end.
13900